\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:es{-}E(${\it es}$).
\\[0ex]($\uparrow$es{-}isconst(${\it es}$; loc($e$); $x$))
\\[0ex]$\Rightarrow$ \=($\forall$$t$,${\it t'}$:rationals.\+
\\[0ex](\=es{-}state{-}ap(es\_state\_when(${\it es}$; $e$); $x$)($t$)\+
\\[0ex]=
\\[0ex]es{-}state{-}ap(es\_state\_when(${\it es}$; $e$); $x$)(${\it t'}$)
\\[0ex]$\in$ es{-}vartype(${\it es}$; loc($e$); $x$))
\-\\[0ex]$\wedge$ (\=es{-}state{-}ap(es\_state\_after(${\it es}$; $e$); $x$)($t$)\+
\\[0ex]=
\\[0ex]es{-}state{-}ap(es\_state\_after(${\it es}$; $e$); $x$)(${\it t'}$)
\\[0ex]$\in$ es{-}vartype(${\it es}$; loc($e$); $x$)))
\-\-
\end{tabbing}